Runtime Complexity (innermost) proof of /tmp/tmpR9OY

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 CdtProblem

↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtKnowledgeProof (⇔, 0 ms)

↳8 CdtProblem

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 120 ms)

↳10 CdtProblem

↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 CdtProblem

↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳16 CdtProblem

↳17 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳18 CdtProblem

↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳20 CdtProblem

↳21 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳22 CdtProblem

↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳24 CdtProblem

↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 CdtProblem

↳27 CdtKnowledgeProof (⇔, 0 ms)

↳28 CdtProblem

↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 30 ms)

↳30 CdtProblem

↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 0 ms)

↳32 CdtProblem

↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)

↳34 CdtProblem

↳35 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳36 CdtProblem

↳37 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳38 CdtProblem

↳39 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳40 CdtProblem

↳41 CdtRewritingProof (BOTH BOUNDS(ID, ID), 0 ms)

↳42 CdtProblem

↳43 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 2 ms)

↳44 CdtProblem

↳45 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 12 ms)

↳46 CdtProblem

↳47 SIsEmptyProof (⇔, 0 ms)

↳48 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

cond(true, x, y) → cond(gr(x, y), p(x), s(y))
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, z0, z1) → c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1), P(z0))
GR(s(z0), s(z1)) → c3(GR(z0, z1))

S tuples:

COND(true, z0, z1) → c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1), P(z0))
GR(s(z0), s(z1)) → c3(GR(z0, z1))

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND(true, z0, z1) → c(COND(gr(z0, z1), p(z0), s(z1)), GR(z0, z1), P(z0)) by

COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, 0, z0) → c(COND(false, p(0), s(z0)), GR(0, z0), P(0))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, x0, x1) → c

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, 0, z0) → c(COND(false, p(0), s(z0)), GR(0, z0), P(0))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, x0, x1) → c

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, 0, z0) → c(COND(false, p(0), s(z0)), GR(0, z0), P(0))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, x0, x1) → c

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c, c

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

COND(true, x0, x1) → c
COND(true, 0, z0) → c(COND(false, p(0), s(z0)), GR(0, z0), P(0))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))

We considered the (Usable) Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(s(z0)) → z0

And the Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND(x₁, x₂, x₃)) = [2]x₂
POL(GR(x₁, x₂)) = 0
POL(P(x₁)) = 0
POL(c(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c3(x₁)) = x₁
POL(false) = [5]
POL(gr(x₁, x₂)) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = [4] + x₁
POL(true) = 0

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND(true, 0, x1) → c(COND(gr(0, x1), 0, s(x1)), GR(0, x1), P(0)) by

COND(true, 0, z0) → c(COND(false, 0, s(z0)), GR(0, z0), P(0))
COND(true, 0, x0) → c

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, 0, z0) → c(COND(false, 0, s(z0)), GR(0, z0), P(0))
COND(true, 0, x0) → c

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, 0, z0) → c(COND(false, 0, s(z0)), GR(0, z0), P(0))
COND(true, 0, x0) → c

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c, c

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

COND(true, 0, x0) → c
COND(true, 0, z0) → c(COND(false, 0, s(z0)), GR(0, z0), P(0))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0))) by

COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(x0), x1) → c

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(x0), x1) → c

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), x1) → c(COND(gr(s(z0), x1), z0, s(x1)), GR(s(z0), x1), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c, c

(17) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))

Removed 1 trailing nodes:

COND(true, s(x0), x1) → c

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0))) by

COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(x0), 0) → c

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))
COND(true, s(x0), 0) → c

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:

COND(true, s(z0), 0) → c(COND(true, p(s(z0)), s(0)), GR(s(z0), 0), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c, c

(21) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND(true, s(z0), 0) → c(COND(true, z0, s(0)), GR(s(z0), 0), P(s(z0)))

Removed 1 trailing nodes:

COND(true, s(x0), 0) → c

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), p(s(z0)), s(s(z1))), GR(s(z0), s(z1)), P(s(z0))) by

COND(true, s(z0), s(x1)) → c(COND(gr(z0, x1), z0, s(s(x1))), GR(s(z0), s(x1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
COND(true, s(x0), s(x1)) → c

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
COND(true, s(x0), s(x1)) → c

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(x1)) → c(COND(gr(z0, x1), z0, s(s(x1))), GR(s(z0), s(x1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
COND(true, s(x0), s(x1)) → c

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c, c

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND(true, s(x0), s(x1)) → c

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(x1)) → c(COND(gr(z0, x1), z0, s(s(x1))), GR(s(z0), s(x1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

K tuples:none
Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(27) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(x1)) → c(COND(gr(z0, x1), z0, s(s(x1))), GR(s(z0), s(x1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))

We considered the (Usable) Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(s(z0)) → z0

And the Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND(x₁, x₂, x₃)) = x₁ + [2]x₃
POL(GR(x₁, x₂)) = 0
POL(P(x₁)) = 0
POL(c(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c3(x₁)) = x₁
POL(false) = 0
POL(gr(x₁, x₂)) = [1]
POL(p(x₁)) = [4]
POL(s(x₁)) = 0
POL(true) = [1]

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(x1)) → c(COND(gr(z0, x1), z0, s(s(x1))), GR(s(z0), s(x1)), P(s(z0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

We considered the (Usable) Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(s(z0)) → z0

And the Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND(x₁, x₂, x₃)) = x₂
POL(GR(x₁, x₂)) = 0
POL(P(x₁)) = 0
POL(c(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c3(x₁)) = x₁
POL(false) = [4]
POL(gr(x₁, x₂)) = 0
POL(p(x₁)) = x₁
POL(s(x₁)) = [4] + x₁
POL(true) = 0

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(z0), s(z1)) → c3(GR(z0, z1))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

GR, COND

Compound Symbols:

c3, c

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace GR(s(z0), s(z1)) → c3(GR(z0, z1)) by

GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

S tuples:

COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(35) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

COND(true, s(0), s(z0)) → c(COND(false, p(s(0)), s(s(z0))), GR(s(0), s(z0)), P(s(0)))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

S tuples:

COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(37) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0)))) by COND(true, s(s(z0)), s(0)) → c(COND(true, s(z0), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(0)) → c(COND(true, s(z0), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))

S tuples:

COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

K tuples:

COND(true, s(s(z0)), s(0)) → c(COND(true, p(s(s(z0))), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))
COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(39) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

COND(true, s(s(z0)), s(0)) → c(COND(true, s(z0), s(s(0))), GR(s(s(z0)), s(0)), P(s(s(z0))))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

S tuples:

COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

K tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(41) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), p(s(s(z0))), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0)))) by COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

K tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(43) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

We considered the (Usable) Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)

And the Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0
POL(COND(x₁, x₂, x₃)) = [2]x₂·x₃ + [2]x₂²
POL(GR(x₁, x₂)) = 0
POL(P(x₁)) = 0
POL(c(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c3(x₁)) = x₁
POL(false) = 0
POL(gr(x₁, x₂)) = 0
POL(s(x₁)) = [1] + x₁
POL(true) = 0

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:

GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

K tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(45) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

We considered the (Usable) Rules:

gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)

And the Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = [2]
POL(COND(x₁, x₂, x₃)) = x₂²
POL(GR(x₁, x₂)) = x₁
POL(P(x₁)) = 0
POL(c(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(c3(x₁)) = x₁
POL(false) = 0
POL(gr(x₁, x₂)) = [2]x₁·x₂
POL(s(x₁)) = [1] + x₁
POL(true) = [2]

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

cond(true, z0, z1) → cond(gr(z0, z1), p(z0), s(z1))
gr(0, z0) → false
gr(s(z0), 0) → true
gr(s(z0), s(z1)) → gr(z0, z1)
p(0) → 0
p(s(z0)) → z0

Tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))

S tuples:none
K tuples:

COND(true, s(z0), s(z1)) → c(COND(gr(z0, z1), z0, s(s(z1))), GR(s(z0), s(z1)), P(s(z0)))
COND(true, s(s(z0)), s(s(z1))) → c(COND(gr(z0, z1), s(z0), s(s(s(z1)))), GR(s(s(z0)), s(s(z1))), P(s(s(z0))))
GR(s(s(y0)), s(s(y1))) → c3(GR(s(y0), s(y1)))

Defined Rule Symbols:

cond, gr, p

Defined Pair Symbols:

COND, GR

Compound Symbols:

c, c3

(47) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtKnowledgeProof (EQUIVALENT transformation)

(8) Obligation:

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(10) Obligation:

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(16) Obligation:

(17) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(18) Obligation:

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(22) Obligation:

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

(24) Obligation:

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(26) Obligation:

(27) CdtKnowledgeProof (EQUIVALENT transformation)

(28) Obligation:

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(30) Obligation:

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

(32) Obligation:

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

(34) Obligation:

(35) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(36) Obligation:

(37) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

(38) Obligation:

(39) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(40) Obligation:

(41) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

(42) Obligation:

(43) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(44) Obligation:

(45) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

(46) Obligation:

(47) SIsEmptyProof (EQUIVALENT transformation)

(48) BOUNDS(O(1), O(1))